$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$${\it as}$, ${\it bs}$:$T$ List. merge(${\it as}$;${\it bs}$) $\in$ $T$ List)